YES 1.058 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule FiniteMap
  ((eltsFM_LE :: FiniteMap Ordering a  ->  Ordering  ->  [a]) :: FiniteMap Ordering a  ->  Ordering  ->  [a])

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  eltsFM_LE :: Ord a => FiniteMap a b  ->  a  ->  [b]
eltsFM_LE fm fr foldFM_LE (\key elt rest ->elt : rest) [] fr fm

  foldFM_LE :: Ord a => (a  ->  b  ->  c  ->  c ->  c  ->  a  ->  FiniteMap a b  ->  c
foldFM_LE k z fr EmptyFM z
foldFM_LE k z fr (Branch key elt _ fm_l fm_r
 | key <= fr = 
foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
 | otherwise = 
foldFM_LE k z fr fm_l


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\keyeltrestelt : rest

is transformed to
eltsFM_LE0 key elt rest = elt : rest



↳ HASKELL
  ↳ LR
HASKELL
      ↳ BR

mainModule FiniteMap
  ((eltsFM_LE :: FiniteMap Ordering a  ->  Ordering  ->  [a]) :: FiniteMap Ordering a  ->  Ordering  ->  [a])

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b


  eltsFM_LE :: Ord a => FiniteMap a b  ->  a  ->  [b]
eltsFM_LE fm fr foldFM_LE eltsFM_LE0 [] fr fm

  
eltsFM_LE0 key elt rest elt : rest

  foldFM_LE :: Ord c => (c  ->  a  ->  b  ->  b ->  b  ->  c  ->  FiniteMap c a  ->  b
foldFM_LE k z fr EmptyFM z
foldFM_LE k z fr (Branch key elt _ fm_l fm_r
 | key <= fr = 
foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
 | otherwise = 
foldFM_LE k z fr fm_l


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule FiniteMap
  ((eltsFM_LE :: FiniteMap Ordering a  ->  Ordering  ->  [a]) :: FiniteMap Ordering a  ->  Ordering  ->  [a])

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  eltsFM_LE :: Ord b => FiniteMap b a  ->  b  ->  [a]
eltsFM_LE fm fr foldFM_LE eltsFM_LE0 [] fr fm

  
eltsFM_LE0 key elt rest elt : rest

  foldFM_LE :: Ord a => (a  ->  b  ->  c  ->  c ->  c  ->  a  ->  FiniteMap a b  ->  c
foldFM_LE k z fr EmptyFM z
foldFM_LE k z fr (Branch key elt vw fm_l fm_r
 | key <= fr = 
foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
 | otherwise = 
foldFM_LE k z fr fm_l


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Cond Reductions:
The following Function with conditions
foldFM_LE k z fr EmptyFM = z
foldFM_LE k z fr (Branch key elt vw fm_l fm_r)
 | key <= fr
 = foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
 | otherwise
 = foldFM_LE k z fr fm_l

is transformed to
foldFM_LE k z fr EmptyFM = foldFM_LE3 k z fr EmptyFM
foldFM_LE k z fr (Branch key elt vw fm_l fm_r) = foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE0 k z fr key elt vw fm_l fm_r True = foldFM_LE k z fr fm_l

foldFM_LE1 k z fr key elt vw fm_l fm_r True = foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
foldFM_LE1 k z fr key elt vw fm_l fm_r False = foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r) = foldFM_LE1 k z fr key elt vw fm_l fm_r (key <= fr)

foldFM_LE3 k z fr EmptyFM = z
foldFM_LE3 wv ww wx wy = foldFM_LE2 wv ww wx wy

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule FiniteMap
  (eltsFM_LE :: FiniteMap Ordering a  ->  Ordering  ->  [a])

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  eltsFM_LE :: Ord b => FiniteMap b a  ->  b  ->  [a]
eltsFM_LE fm fr foldFM_LE eltsFM_LE0 [] fr fm

  
eltsFM_LE0 key elt rest elt : rest

  foldFM_LE :: Ord a => (a  ->  b  ->  c  ->  c ->  c  ->  a  ->  FiniteMap a b  ->  c
foldFM_LE k z fr EmptyFM foldFM_LE3 k z fr EmptyFM
foldFM_LE k z fr (Branch key elt vw fm_l fm_rfoldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

  
foldFM_LE0 k z fr key elt vw fm_l fm_r True foldFM_LE k z fr fm_l

  
foldFM_LE1 k z fr key elt vw fm_l fm_r True foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
foldFM_LE1 k z fr key elt vw fm_l fm_r False foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise

  
foldFM_LE2 k z fr (Branch key elt vw fm_l fm_rfoldFM_LE1 k z fr key elt vw fm_l fm_r (key <= fr)

  
foldFM_LE3 k z fr EmptyFM z
foldFM_LE3 wv ww wx wy foldFM_LE2 wv ww wx wy


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE1(wz13, EQ, wz341, wz342, wz343, wz344, h) → new_foldFM_LE3(wz13, wz343, h)
new_foldFM_LE4(wz31, wz10, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE1(new_eltsFM_LE01(wz31, wz10, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE2(wz31, wz9, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE1(new_eltsFM_LE00(wz31, wz9, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE1(wz13, GT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE3(wz13, wz343, h)
new_foldFM_LE1(wz13, EQ, wz341, wz342, wz343, wz344, h) → new_foldFM_LE2(wz341, new_foldFM_LE0(wz13, wz343, h), wz344, h)
new_foldFM_LE1(wz13, LT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE(wz341, new_foldFM_LE0(wz13, wz343, h), wz344, h)
new_foldFM_LE1(wz13, GT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE4(wz341, new_foldFM_LE0(wz13, wz343, h), wz344, h)
new_foldFM_LE(wz31, wz7, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE1(new_eltsFM_LE0(wz31, wz7, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE3(wz13, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE1(wz13, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE1(wz13, LT, wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, h) → new_foldFM_LE1(wz13, wz3430, wz3431, wz3432, wz3433, wz3434, h)

The TRS R consists of the following rules:

new_foldFM_LE5(wz31, wz9, EmptyFM, h) → new_eltsFM_LE00(wz31, wz9, h)
new_foldFM_LE6(wz31, wz7, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE10(new_eltsFM_LE0(wz31, wz7, h), wz340, wz341, wz342, wz343, wz344, h)
new_eltsFM_LE0(wz31, wz5, h) → :(wz31, wz5)
new_foldFM_LE0(wz13, EmptyFM, h) → wz13
new_eltsFM_LE01(wz31, wz10, h) → :(wz31, wz10)
new_foldFM_LE7(wz31, wz10, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE10(new_eltsFM_LE01(wz31, wz10, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE10(wz13, GT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE7(wz341, new_foldFM_LE0(wz13, wz343, h), wz344, h)
new_eltsFM_LE00(wz31, wz8, h) → :(wz31, wz8)
new_foldFM_LE6(wz31, wz7, EmptyFM, h) → new_eltsFM_LE0(wz31, wz7, h)
new_foldFM_LE5(wz31, wz9, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE10(new_eltsFM_LE00(wz31, wz9, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE7(wz31, wz10, EmptyFM, h) → new_eltsFM_LE01(wz31, wz10, h)
new_foldFM_LE10(wz13, LT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE6(wz341, new_foldFM_LE0(wz13, wz343, h), wz344, h)
new_foldFM_LE0(wz13, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE10(wz13, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE10(wz13, EQ, wz341, wz342, wz343, wz344, h) → new_foldFM_LE5(wz341, new_foldFM_LE0(wz13, wz343, h), wz344, h)

The set Q consists of the following terms:

new_foldFM_LE10(x0, GT, x1, x2, x3, x4, x5)
new_foldFM_LE10(x0, EQ, x1, x2, x3, x4, x5)
new_foldFM_LE10(x0, LT, x1, x2, x3, x4, x5)
new_foldFM_LE7(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE0(x0, Branch(x1, x2, x3, x4, x5), x6)
new_eltsFM_LE00(x0, x1, x2)
new_foldFM_LE0(x0, EmptyFM, x1)
new_eltsFM_LE01(x0, x1, x2)
new_foldFM_LE7(x0, x1, EmptyFM, x2)
new_eltsFM_LE0(x0, x1, x2)
new_foldFM_LE6(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE6(x0, x1, EmptyFM, x2)
new_foldFM_LE5(x0, x1, EmptyFM, x2)
new_foldFM_LE5(x0, x1, Branch(x2, x3, x4, x5, x6), x7)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE11(wz12, EQ, wz341, wz342, wz343, wz344, h) → new_foldFM_LE13(wz12, wz343, h)
new_foldFM_LE11(wz12, GT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE13(wz12, wz343, h)
new_foldFM_LE13(wz12, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE11(wz12, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE11(wz12, LT, wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, h) → new_foldFM_LE11(wz12, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE11(wz12, LT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE8(wz341, new_foldFM_LE9(wz12, wz343, h), wz344, h)
new_foldFM_LE11(wz12, EQ, wz341, wz342, wz343, wz344, h) → new_foldFM_LE12(wz341, new_foldFM_LE9(wz12, wz343, h), wz344, h)
new_foldFM_LE12(wz31, wz8, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE11(new_eltsFM_LE00(wz31, wz8, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE8(wz31, wz6, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE11(new_eltsFM_LE0(wz31, wz6, h), wz340, wz341, wz342, wz343, wz344, h)

The TRS R consists of the following rules:

new_eltsFM_LE00(wz31, wz8, h) → :(wz31, wz8)
new_foldFM_LE14(wz12, EQ, wz341, wz342, wz343, wz344, h) → new_foldFM_LE16(wz341, new_foldFM_LE9(wz12, wz343, h), wz344, h)
new_eltsFM_LE0(wz31, wz5, h) → :(wz31, wz5)
new_foldFM_LE16(wz31, wz8, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE14(new_eltsFM_LE00(wz31, wz8, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE14(wz12, LT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE15(wz341, new_foldFM_LE9(wz12, wz343, h), wz344, h)
new_foldFM_LE16(wz31, wz8, EmptyFM, h) → new_eltsFM_LE00(wz31, wz8, h)
new_foldFM_LE9(wz12, EmptyFM, h) → wz12
new_foldFM_LE15(wz31, wz6, EmptyFM, h) → new_eltsFM_LE0(wz31, wz6, h)
new_foldFM_LE9(wz12, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE14(wz12, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE15(wz31, wz6, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE14(new_eltsFM_LE0(wz31, wz6, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE14(wz12, GT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE9(wz12, wz343, h)

The set Q consists of the following terms:

new_foldFM_LE14(x0, GT, x1, x2, x3, x4, x5)
new_foldFM_LE16(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE9(x0, Branch(x1, x2, x3, x4, x5), x6)
new_foldFM_LE15(x0, x1, EmptyFM, x2)
new_foldFM_LE14(x0, LT, x1, x2, x3, x4, x5)
new_foldFM_LE16(x0, x1, EmptyFM, x2)
new_eltsFM_LE00(x0, x1, x2)
new_foldFM_LE9(x0, EmptyFM, x1)
new_foldFM_LE15(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE14(x0, EQ, x1, x2, x3, x4, x5)
new_eltsFM_LE0(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE17(wz11, LT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE18(wz341, new_foldFM_LE19(wz11, wz343, h), wz344, h)
new_foldFM_LE17(wz11, LT, wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, h) → new_foldFM_LE17(wz11, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE17(wz11, EQ, wz341, wz342, wz343, wz344, h) → new_foldFM_LE20(wz11, wz343, h)
new_foldFM_LE18(wz31, wz5, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE17(new_eltsFM_LE0(wz31, wz5, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE20(wz11, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE17(wz11, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE17(wz11, GT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE20(wz11, wz343, h)

The TRS R consists of the following rules:

new_foldFM_LE19(wz11, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE110(wz11, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE110(wz11, GT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE19(wz11, wz343, h)
new_foldFM_LE21(wz31, wz5, EmptyFM, h) → new_eltsFM_LE0(wz31, wz5, h)
new_eltsFM_LE0(wz31, wz5, h) → :(wz31, wz5)
new_foldFM_LE110(wz11, LT, wz341, wz342, wz343, wz344, h) → new_foldFM_LE21(wz341, new_foldFM_LE19(wz11, wz343, h), wz344, h)
new_foldFM_LE110(wz11, EQ, wz341, wz342, wz343, wz344, h) → new_foldFM_LE19(wz11, wz343, h)
new_foldFM_LE19(wz11, EmptyFM, h) → wz11
new_foldFM_LE21(wz31, wz5, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE110(new_eltsFM_LE0(wz31, wz5, h), wz340, wz341, wz342, wz343, wz344, h)

The set Q consists of the following terms:

new_foldFM_LE21(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE19(x0, Branch(x1, x2, x3, x4, x5), x6)
new_foldFM_LE19(x0, EmptyFM, x1)
new_foldFM_LE110(x0, LT, x1, x2, x3, x4, x5)
new_foldFM_LE21(x0, x1, EmptyFM, x2)
new_foldFM_LE110(x0, EQ, x1, x2, x3, x4, x5)
new_foldFM_LE110(x0, GT, x1, x2, x3, x4, x5)
new_eltsFM_LE0(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE22(EQ, Branch(LT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(EQ, wz33, h)
new_foldFM_LE22(GT, Branch(LT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(GT, wz33, h)
new_foldFM_LE22(EQ, Branch(GT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(EQ, wz33, h)
new_foldFM_LE22(LT, Branch(EQ, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(LT, wz33, h)
new_foldFM_LE22(LT, Branch(LT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(LT, wz33, h)
new_foldFM_LE22(GT, Branch(EQ, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(GT, wz33, h)
new_foldFM_LE22(LT, Branch(GT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(LT, wz33, h)
new_foldFM_LE22(EQ, Branch(EQ, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(EQ, wz33, h)
new_foldFM_LE22(GT, Branch(GT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(GT, wz33, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE22(LT, Branch(EQ, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(LT, wz33, h)
new_foldFM_LE22(LT, Branch(LT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(LT, wz33, h)
new_foldFM_LE22(LT, Branch(GT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(LT, wz33, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE22(GT, Branch(LT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(GT, wz33, h)
new_foldFM_LE22(GT, Branch(EQ, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(GT, wz33, h)
new_foldFM_LE22(GT, Branch(GT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(GT, wz33, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE22(EQ, Branch(GT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(EQ, wz33, h)
new_foldFM_LE22(EQ, Branch(LT, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(EQ, wz33, h)
new_foldFM_LE22(EQ, Branch(EQ, wz31, wz32, wz33, wz34), h) → new_foldFM_LE22(EQ, wz33, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: